 Process
Analysis Toolkit (PAT) 3.5
Help |
Since PRTS is a combination of PCSP and RTS, then it
inherites all the syntax of these two modules. Besides all the process
definitions in CSP#, PRTS also has keywords such as pcase, Wait, within and so on. Although
no new keyword is introduced, the combination of
process definitions from different modules makes the model more
meaningful. Following is a small example: P = (pcase {
[prob1] : Wait[d1]; Q1
[prob2] : (Q2)within[d2]
...
default : Qn interrupt[dn]
Qn+1
})deadline[d]; //note: here we can also use weighted pcase for convenience, just as
in PCSP. This process means process P should finish in d time
units(deadline[d]); and meanwhile, according to the
transition probability P has probabilistic choices to different
processes such as Wait[d1]; Q1 or (Q2)within[d2]. Notice that Qi could also have
real-time and probabilistic transition itself. Remark: The following
language constructs are also disallowed in probabilistic real-time system
model. This is the same as RTS module because these two commands will
generate conflicitions with implicit clocks we use. [b]P ifa
(b) {P} else
{Q}
Copyright © 2007-2012 Semantic Engineering Pte. Ltd.